/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package alloytoy;

import edu.mit.csail.sdg.alloy4.*;
import java.util.*;

/**
 * A A4Reporter class.
 * @author Daniel
 */
public final class MyReporter extends A4Reporter {

    private int warningCount=0;
    private ArrayList<String> Warnings;

    public MyReporter(){
        Warnings = new ArrayList<String>();
    }

    public int getWarningCount(){
        return warningCount;
    }

    public ArrayList<String> getWarnings(){
        return Warnings;
    }

    @Override public void warning(final ErrorWarning e) {
        warningCount++;
        // the location is in "e.pos"
        //System.out.println("Warning #"+warningCount);
        //System.out.println(e.msg.trim());
        Warnings.add(e.toString());
    }

    @Override public void translate
    (String solver, int bitwidth,
    int maxseq, int skolemDepth, int symmetry) {
        System.out.println("Solver="+solver
             +" Bitwidth="+bitwidth
             +" MaxSeq="+maxseq
             +(skolemDepth==0?"":" SkolemDepth="+skolemDepth)
             +" Symmetry="+(symmetry>0 ? (""+symmetry) : "OFF")
             +"\nGenerating CNF...\n"
        );
    }

    @Override public void solve
    (int primaryVars, int totalVars, int clauses) {
        System.out.println("Var="+totalVars
             +" PrimaryVars="+primaryVars
             +" Clauses="+clauses
             +"\nSolving...\n"
             );
    }

    @Override public void resultCNF(final String filename) {
        System.out.println("CNF file written to "+filename+"\n");
    }

    /*@Override public void resultSAT(Object command, long solvingTime, String filename) {
        Command cmd = (Command)command;
        if (cmd.check) {
          System.out.println("Counterexample found.");
          System.out.println("Assertion is invalid");
        } else {
          System.out.println("Instance found.");
          System.out.println("Predicate is consistent");
        }
        if (cmd.expects==0) System.out.println(", contrary to expectation");
        else if (cmd.expects==1) System.out.println(", as expected");
        System.out.println(""+solvingTime+"ms.");
    }

    @Override public void resultUNSAT (Object command, long solvingTime, String filename) {
        Command cmd = (Command)command;
        if (cmd.check) {
            System.out.println("No counterexample found.");
            System.out.println("Assertion may be valid");
        } else {
            System.out.println("No instance found.");
            System.out.println(" Predicate may be inconsistent");
        }
        if (cmd.expects==1) System.out.println(", contrary to expectation");
        else if (cmd.expects==0) System.out.println(", as expected");
        System.out.println(""+solvingTime+"ms.\n\n");
    }*/
}
